$\forall$$T$:Type, $A$,$B$:($T$ List), $x$,$y$:$T$.
\\[0ex]l\_before($x$; $y$; append($A$; $B$); $T$)
\\[0ex]$\Leftarrow\!\Rightarrow$ (l\_before($x$; $y$; $A$; $T$) $\vee$ l\_before($x$; $y$; $B$; $T$) $\vee$ (($x$ $\in$ $A$) $\wedge$ ($y$ $\in$ $B$)))